Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		pred(s(x))	→ x
2:		minus(x,0)	→ x
3:		minus(x,s(y))	→ pred(minus(x,y))
4:		quot(0,s(y))	→ 0
5:		quot(s(x),s(y))	→ s(quot(minus(x,y),s(y)))
6:		log(s(0))	→ 0
7:		log(s(s(x)))	→ s(log(s(quot(x,s(s(0))))))

There are 6 dependency pairs:


8:		MINUS(x,s(y))	→ PRED(minus(x,y))
9:		MINUS(x,s(y))	→ MINUS(x,y)
10:		QUOT(s(x),s(y))	→ QUOT(minus(x,y),s(y))
11:		QUOT(s(x),s(y))	→ MINUS(x,y)
12:		LOG(s(s(x)))	→ LOG(s(quot(x,s(s(0)))))
13:		LOG(s(s(x)))	→ QUOT(x,s(s(0)))

The approximated dependency graph contains 3 SCCs: {9}, {10} and {12}.

Consider the SCC {9}. There are no usable rules. By taking the AF π with π(MINUS) = 2 together with the lexicographic path order with empty precedence, rule 9 is strictly decreasing.

Consider the SCC {10}. The usable rules are {1-3}. By taking the AF π with π(minus) = π(pred) = π(QUOT) = 1 together with the lexicographic path order with empty precedence, the rules in {2,3} are weakly decreasing and the rules in {1,10} are strictly decreasing.

Consider the SCC {12}. The usable rules are {1-5}. By taking the AF π with π(LOG) = π(minus) = π(pred) = π(quot) = 1 together with the lexicographic path order with empty precedence, the rules in {2-5} are weakly decreasing and the rules in {1,12} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.04 seconds) --- May 4, 2006